$\forall$$T$, ${\it T'}$:Type$_{\mbox{\scriptsize i}}$, $f$:($T$$\rightarrow$${\it T'}$), $L$:$T$ List, $P$:(${\it T'}$$\rightarrow$${\it T'}$$\rightarrow$Prop$_{\mbox{\scriptsize i'}}$).
\\[0ex]($\forall$$x$,$y$$\in$map($f$;$L$).$P$($x$,$y$)) $\Leftrightarrow$ ($\forall$$x$,$y$$\in$$L$.$P$($f$($x$),$f$($y$)))